a, b, c:.
(a  b)
 (b  c)
 (E:({a..c}). a  j < c. E(j) = (a  j < b. E(j) + b  j < c. E(j))  ) 

latex

Definitions	t  T, t.2, t.1, CRng, <+*>, +r, x f y, |r|, x:A. B(x), a  j < b. E(j)
Lemmas	crng wf, qrng wf, rng sum split